Search Results

Documents authored by Murano, Aniello

Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2024
LIPIcs, Volume 288, CSL 2024, Complete Volume

Authors: Aniello Murano and Alexandra Silva

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
LIPIcs, Volume 288, CSL 2024, Complete Volume
Cite as

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1-892, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{murano_et_al:LIPIcs.CSL.2024,
  title =	{{LIPIcs, Volume 288, CSL 2024, Complete Volume}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{1--892},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024},
  URN =		{urn:nbn:de:0030-drops-196423},
  doi =		{10.4230/LIPIcs.CSL.2024},
  annote =	{Keywords: LIPIcs, Volume 288, CSL 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Aniello Murano and Alexandra Silva

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{murano_et_al:LIPIcs.CSL.2024.0,
  author =	{Murano, Aniello and Silva, Alexandra},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.0},
  URN =		{urn:nbn:de:0030-drops-196436},
  doi =		{10.4230/LIPIcs.CSL.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TIME.2018.6
Results on Alternating-Time Temporal Logics with Linear Past

Authors: Laura Bozzelli, Aniello Murano, and Loredana Sorrentino

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

Abstract
We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard CTL^* (resp., ATL^*). We establish by formal non-trivial arguments that the "memoryful" linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard "local" linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL-like fragment, denoted ATL_{lp}, of the known "memoryful" linear-past extension of ATL^{*}. We show that ATL_{lp} is strictly more expressive than ATL, and interestingly, it can be exponentially more succinct than the more expressive logic ATL^{*}. Moreover, we prove that both satisfiability and model-checking for the logic ATL_{lp} are Exptime-complete.
Cite as

Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. Results on Alternating-Time Temporal Logics with Linear Past. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2018.6,
  author =	{Bozzelli, Laura and Murano, Aniello and Sorrentino, Loredana},
  title =	{{Results on Alternating-Time Temporal Logics with Linear Past}},
  booktitle =	{25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-089-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{120},
  editor =	{Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.6},
  URN =		{urn:nbn:de:0030-drops-97714},
  doi =		{10.4230/LIPIcs.TIME.2018.6},
  annote =	{Keywords: Alternating-time temporal logics, Linear Past, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.23
Quantifying Bounds in Strategy Logic

Authors: Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.
Cite as

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying Bounds in Strategy Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.CSL.2018.23,
  author =	{Fijalkow, Nathana\"{e}l and Maubert, Bastien and Murano, Aniello and Rubin, Sasha},
  title =	{{Quantifying Bounds in Strategy Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{23:1--23:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.23},
  URN =		{urn:nbn:de:0030-drops-96901},
  doi =		{10.4230/LIPIcs.CSL.2018.23},
  annote =	{Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.6
Hierarchical Cost-Parity Games

Authors: Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.
Cite as

Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. Hierarchical Cost-Parity Games. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2017.6,
  author =	{Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},
  title =	{{Hierarchical Cost-Parity Games}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.6},
  URN =		{urn:nbn:de:0030-drops-79175},
  doi =		{10.4230/LIPIcs.TIME.2017.6},
  annote =	{Keywords: Parity Games, Cost-Parity Games, Hierarchical Systems, System Verification}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.11
Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking

Authors: Dario Della Monica, David de Frutos-Escrig, Angelo Montanari, Aniello Murano, and Guido Sciavicco

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
The problem of temporal dataset evaluation consists in establishing to what extent a set of temporal data (histories) complies with a given temporal condition. It presents a strong resemblance with the problem of model checking enhanced with the ability of rating the compliance degree of a model against a formula. In this paper, we solve the temporal dataset evaluation problem by suitably combining the outcomes of model checking an interval temporal logic formula against sets of histories (finite interval models), possibly taking into account domain-dependent measures/criteria, like, for instance, sensitivity, specificity, and accuracy. From a technical point of view, the main contribution of the paper is a (deterministic) polynomial time algorithm for interval temporal logic model checking over finite interval models. To the best of our knowledge, this is the first application of a (truly) interval temporal logic model checking in the area of temporal databases and data mining rather than in the formal verification setting.
Cite as

Dario Della Monica, David de Frutos-Escrig, Angelo Montanari, Aniello Murano, and Guido Sciavicco. Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dellamonica_et_al:LIPIcs.TIME.2017.11,
  author =	{Della Monica, Dario and de Frutos-Escrig, David and Montanari, Angelo and Murano, Aniello and Sciavicco, Guido},
  title =	{{Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.11},
  URN =		{urn:nbn:de:0030-drops-79280},
  doi =		{10.4230/LIPIcs.TIME.2017.11},
  annote =	{Keywords: Dataset Evaluation, Temporal Databases, Model Checking, Interval Temporal Logics}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.133
Reasoning About Strategies

Authors: Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between open entities and express that the system is correct no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by SL-CHP, with the aim of getting a powerful framework for reasoning explicitly about strategies. SL-CHP is obtained by using first-order quantifications over strategies and it has been investigated in the specific setting of two-agents turn-based game structures where a non-elementary model-checking algorithm has been provided. While SL-CHP is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about strategies in multi-agent concurrent systems. We prove that SL strictly includes SL-CHP, while maintaining a decidable model-checking problem. Indeed, we show that it is 2ExpTime-complete, thus not harder than that for ATL* and a remarkable improvement of the same problem for SL-CHP. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic SL-CHP under the concurrent game semantics.
Cite as

Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning About Strategies. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 133-144, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{mogavero_et_al:LIPIcs.FSTTCS.2010.133,
  author =	{Mogavero, Fabio and Murano, Aniello and Vardi, Moshe Y.},
  title =	{{Reasoning About Strategies}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{133--144},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.133},
  URN =		{urn:nbn:de:0030-drops-28597},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.133},
  annote =	{Keywords: open systems, multi-agent systems, verification, strategy quantifier, alternating temporal logic, model-checking}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact